home *** CD-ROM | disk | FTP | other *** search
/ Turnbull China Bikeride / Turnbull China Bikeride - Disc 2.iso / STUTTGART / LANG / PROLOG / HUMBOLT / HUMBOLTS / _files / _humboltsr / ARITH._c next >
Text File  |  1990-08-19  |  33KB  |  1,137 lines
  1.  
  2. /***************************************************
  3. ****************************************************
  4. **                                                **
  5. **  HU-Prolog     Portable Interpreter System     ** 
  6. **                                                **
  7. **  Release 1.62   January  1990                  **
  8. **                                                **
  9. **  Authors:      C.Horn, M.Dziadzka, M.Horn      **
  10. **                                                **
  11. **  (C) 1988      Humboldt-University             **
  12. **                Department of Mathematics       **
  13. **                GDR 1086 Berlin, P.O.Box 1297   **
  14. **                                                **
  15. ****************************************************
  16. ***************************************************/
  17.  
  18. #include "systems.h"
  19. #include "types.h"
  20. #include "errors.h"
  21. #include "atoms.h"
  22.  
  23. #if REALARITH
  24. IMPORT REAL exp(),log(),log10(),sqrt();  /* from mathlib   */
  25. IMPORT REAL sin(),cos(),tan(),atan();    /* from mathlib   */
  26. IMPORT REAL acos(),atan(),floor(),ceil();/* from mathlib   */ 
  27. IMPORT REAL pow(),asin();                /* from mathlib   */
  28. #endif
  29. IMPORT void notecl(),destroycl();
  30. IMPORT boolean UNIFY(),INTRES(),LONGRES();
  31. IMPORT TERM A0,A1,BE;                    /* from evalpreds.c*/
  32. IMPORT boolean DOEQUAL();                /* from evalpreds.c*/
  33. IMPORT ATOM LOOKATOM();                  /* from atomtable.c*/
  34. IMPORT ENV E;                            /* from unify.c */
  35. IMPORT void freeterms();                 /* from manager.c */
  36. IMPORT void ARGERROR(),ERROR();          /* from linebufffer.c */
  37. IMPORT void WRITEOUT();                  /* from writeout.c */
  38. IMPORT TERM SKELETON();                  /* from database.c */
  39. IMPORT int VARCT,VARTOP;                 /* from database.c  */
  40. IMPORT TERM GLOTOP,HEAPTOP;              /* from manager.c  */
  41. IMPORT boolean LONGRES(),testheap();
  42. IMPORT ATOM copyatom();
  43. IMPORT CLAUSE ADDCLAUSE();
  44. IMPORT TERM CALLX;
  45. IMPORT boolean REDUCEFLAG;
  46. IMPORT ATOM modify();
  47.  
  48. #if SYMBOLARITH
  49. FORWARD TERM substsim(),symbred(),pind3_red(),of_red();
  50. #endif
  51. /*
  52. EXPORT int INTVALUE(TERM);
  53. EXPORT boolean DODASS(),DOACOMP(),DOIS();
  54. EXPORT boolean FpAbort,DOREDUCE();
  55. EXPORT TERM DOEVAL();
  56. */
  57.  
  58. #if REALARITH
  59. #define PI_CONST           3.1415926535
  60. #define E_CONST            2.7182818284
  61. #if VMS
  62. boolean FpAbort;
  63. #endif
  64. #endif
  65.  
  66.  
  67. LOCAL int ISDEPTH=0;
  68.  
  69. /* finite state evaluation of arithmetic expressions */
  70. /* arithmetic-stack is placed on global stack */
  71.  
  72. #if REALARITH && LONGARITH
  73. typedef struct { boolean ir;
  74.                  union { REAL rrec; LONG lrec; }arithvalue;
  75.                } ARITHTYPE;
  76. #define isreal(av)         ((av)->ir)
  77. #define realf(av)          ((av)->arithvalue.rrec)
  78. #define longf(av)          ((av)->arithvalue.lrec)
  79.  
  80. LOCAL LONG lis(ARITHTYPE *AT)
  81. { if(isreal(AT)){ISDEPTH=0;ERROR(STDFUNCARGE);}return longf(AT); }
  82. LOCAL REAL ris(ARITHTYPE *AT)
  83. { if(isreal(AT)) return realf(AT); else return (REAL)longf(AT); }
  84. #endif
  85.  
  86. #if REALARITH && ! LONGARITH
  87. typedef struct { boolean ir;
  88.                  union { REAL rrec; int lrec; }arithvalue;
  89.                } ARITHTYPE;
  90. #define isreal(av)         ((av)->ir)
  91. #define realf(av)          ((av)->arithvalue.rrec)
  92. #define longf(av)          ((av)->arithvalue.lrec)
  93.  
  94. LOCAL int lis(ARITHTYPE *AT)
  95. { if(isreal(AT)){ISDEPTH=0;ERROR(STDFUNCARGE);}return longf(AT); }
  96. LOCAL REAL ris(ARITHTYPE *AT)
  97. { if(isreal(AT)) return realf(AT); else return (REAL)longf(AT); }
  98. #endif
  99.  
  100. #if !REALARITH && LONGARITH
  101. typedef LONG ARITHTYPE;
  102. #define longf(av)          (*av)
  103. #define lis(at)            longf(at)
  104. #endif
  105.  
  106. #if !REALARITH && !LONGARITH
  107. typedef int ARITHTYPE;
  108. #define longf(av)         (*av)
  109. #define lis(at)           longf(at)
  110. #endif
  111.  
  112. LOCAL boolean assign(ARITHTYPE *ap, TERM t)
  113. { ATOM A;
  114.              A=name(t);
  115.  
  116. #if LONGARITH
  117.              if(A==INTT) longf(ap)= (LONG)ival(t);
  118.              else if(A==LONGT) longf(ap)=longval(t);
  119. #endif
  120. #if ! LONGARITH
  121.              if(A==INTT) longf(ap)=ival(t);
  122. #endif
  123. #if REALARITH
  124.              else if(A==REALT)
  125.               { realf(ap)=realval(t);isreal(ap)=true; }
  126. #endif
  127.              else return false;
  128.            return true;
  129. }
  130.  
  131. /* compute evaluates operation A on args *at1 and *at2 */
  132. /* the result is in *ap                                */
  133. LOCAL boolean compute(ATOM A, ARITHTYPE *at1, ARITHTYPE *at2, 
  134.                       ARITHTYPE *ap, boolean stdfunc)
  135. {
  136. #if REALARITH
  137.   isreal(ap)=false;
  138. switch(A)
  139. {
  140. case MAXAR_0: longf(ap)= (long)MAXARITY;goto intret;
  141. case MAXDEP_0: longf(ap)= (long)MAXDEPTH;goto intret;
  142. #if LONGARITH
  143. case MAXINT_0: longf(ap)=maxlong;goto intret;
  144. case MININT_0: longf(ap)=minlong;goto intret;
  145. #endif
  146. #if !LONGARITH
  147. case MAXINT_0: longf(ap)=maxint;goto intret;
  148. case MININT_0: longf(ap)=minint;goto intret;
  149. #endif
  150. case PLUS_2: if(isreal(at1)||isreal(at2))
  151.               {realf(ap)=ris(at1) + ris(at2); goto realret;}
  152.               longf(ap)=lis(at1) + lis(at2); goto intret;
  153. case MINUS_2: if(isreal(at1)||isreal(at2))
  154.                {realf(ap)=ris(at1) - ris(at2); goto realret;}
  155.                longf(ap)=lis(at1) - lis(at2); goto intret;
  156. case TIMES_2: if(isreal(at1)||isreal(at2))
  157.                 {realf(ap)=ris(at1) * ris(at2); goto realret;}
  158.                 longf(ap)=lis(at1) * lis(at2); goto intret;
  159. case DIVIDE_2: if(ris(at2)==0.0)ERROR(DIV0E);
  160.                 realf(ap)=ris(at1) / ris(at2); goto realret;
  161. case MINUS_1: if(isreal(at1)){realf(ap)= -ris(at1); goto realret;}
  162.                longf(ap)= -lis(at1); goto intret;
  163. case PI_0:       realf(ap)=PI_CONST;goto realret;
  164. case E_0:        realf(ap)=E_CONST;goto realret;
  165. case REAL_1:     realf(ap)=ris(at1); goto realret;
  166. case EXP_1:      realf(ap)=exp(ris(at1)); goto realret;
  167. case LN_1:       realf(ap)=log(ris(at1)); goto realret;
  168. case LOG10_1:    realf(ap)=log10(ris(at1)); goto realret;
  169. case SQRT_1:     realf(ap)=sqrt(ris(at1)); goto realret;
  170. case SIN_1:      realf(ap)=sin(ris(at1)); goto realret;
  171. case COS_1:      realf(ap)=cos(ris(at1)); goto realret;
  172. case TAN_1:      realf(ap)=tan(ris(at1)); goto realret;
  173. case ASIN_1:     realf(ap)=asin(ris(at1)); goto realret;
  174. case ACOS_1:     realf(ap)=acos(ris(at1)); goto realret;
  175. case ATAN_1:     realf(ap)=atan(ris(at1)); goto realret;
  176. case FLOOR_1:    realf(ap)=floor(ris(at1)); goto realret;
  177. case CEIL_1:     realf(ap)=ceil(ris(at1)); goto realret;
  178. case POWER_2:    realf(ap)=pow(ris(at1),ris(at2)); goto realret;
  179. case LSHIFT_2:   longf(ap)=lis(at1) << lis(at2); goto intret;
  180. case RSHIFT_2:   longf(ap)=lis(at1) >> lis(at2); goto intret;
  181. case BITAND_2:   longf(ap)=lis(at1) & lis(at2); goto intret;
  182. case BITOR_2:    longf(ap)=lis(at1) | lis(at2); goto intret;
  183. case BITNEG_1:   longf(ap)= ~lis(at1); goto intret;
  184. case AND_2:      longf(ap)=lis(at1) && lis(at2); goto intret;
  185. case OR_2:       longf(ap)=lis(at1) || lis(at2); goto intret;
  186. case NEG_1:      longf(ap)= !lis(at1); goto intret;
  187. #if LONGARITH
  188. case ENTIER_1:   longf(ap)= (LONG)floor(ris(at1)); goto intret;
  189. #endif
  190. #if ! LONGARITH
  191. case ENTIER_1:   longf(ap)= (int)floor(ris(at1)); goto intret;
  192. #endif
  193. case IDIV_2: if(lis(at2)==0l)ERROR(DIV0E);
  194.                  longf(ap)=lis(at1) / lis(at2); goto intret;
  195. case MOD_2:  if(lis(at2)==0l)ERROR(DIV0E);
  196.                 longf(ap)=lis(at1) % lis(at2); goto intret;
  197. default: 
  198.                 if(stdfunc)ERROR(UNDEFFUNCE);
  199.                 return false;
  200. }
  201. realret: isreal(ap)=true;
  202. intret:  return true;
  203. #endif
  204. #if ! REALARITH
  205. switch(A)
  206. {
  207. case MAXAR_0: longf(ap)= (long)MAXARITY;goto intret;
  208. case MAXDEP_0: longf(ap)= (long)MAXDEPTH;goto intret;
  209. #if LONGARITH
  210. case MAXINT_0: longf(ap)=maxlong;goto intret;
  211. case MININT_0: longf(ap)=minlong;goto intret;
  212. #endif
  213. #if !LONGARITH
  214. case MAXINT_0: longf(ap)=maxint;goto intret;
  215. case MININT_0: longf(ap)=minint;goto intret;
  216. #endif
  217. case PLUS_2:     longf(ap)=lis(at1) + lis(at2); goto intret;
  218. case MINUS_2:    longf(ap)=lis(at1) - lis(at2); goto intret;
  219. case TIMES_2:    longf(ap)=lis(at1) * lis(at2); goto intret;
  220. case MINUS_1:    longf(ap)= -lis(at1); goto intret;
  221. case LSHIFT_2:   longf(ap)=lis(at1) << lis(at2); goto intret;
  222. case RSHIFT_2:   longf(ap)=lis(at1) >> lis(at2); goto intret;
  223. case BITAND_2:   longf(ap)=lis(at1) & lis(at2); goto intret;
  224. case BITOR_2:    longf(ap)=lis(at1) | lis(at2); goto intret;
  225. case BITNEG_1:   longf(ap)= ~lis(at1); goto intret;
  226. case AND_2:      longf(ap)=lis(at1) && lis(at2); goto intret;
  227. case OR_2:       longf(ap)=lis(at1) || lis(at2); goto intret;
  228. case NEG_1:      longf(ap)= !lis(at1); goto intret;
  229. case IDIV_2:     if(lis(at2)==0l)ERROR(DIV0E);
  230.                  longf(ap)=lis(at1) / lis(at2); goto intret;
  231. case MOD_2:      if(lis(at2)==0l)ERROR(DIV0E);
  232.                  longf(ap)=lis(at1) % lis(at2); goto intret;
  233. default: 
  234.                 if(stdfunc)ERROR(UNDEFFUNCE);
  235.                 return false;
  236. }
  237. intret:  return true;
  238. #endif
  239. }
  240.  
  241. GLOBAL boolean DOREDUCE(TERM B0, TERM B1, boolean eval)
  242. { ATOM A;
  243.   TERM T1,T2;
  244.   ARITHTYPE atR,at1,at2;
  245. #if REALARITH
  246.    isreal(&at1)=isreal(&at2)=false;
  247. #endif
  248.    /* deref(B1); only if eval */
  249.    A=name(B1);
  250.    if(A < FUNCNAME)goto notreduce;
  251.   
  252.    if(A==QUOTE_1){B1=arg1(B1);goto termreduce;}
  253.    switch(A)
  254.    { 
  255.     case PLUS_2: case MINUS_2: case TIMES_2: 
  256.     case LSHIFT_2: case RSHIFT_2: case BITAND_2:
  257.     case BITOR_2: case AND_2: case OR_2: case IDIV_2: case MOD_2:  
  258. #if REALARITH
  259.     case DIVIDE_2: case POWER_2: 
  260. #endif  
  261.              T2=arg2(B1);
  262.              if(!assign(&at2,T2)) goto notreduce;
  263.     
  264.     case MINUS_1: case BITNEG_1: case NEG_1: 
  265. #if REALARITH
  266.     case FLOOR_1: case CEIL_1: case ENTIER_1: case EXP_1:
  267.     case LN_1: case LOG10_1: case SQRT_1: case SIN_1: 
  268.     case COS_1: case TAN_1: case ASIN_1: case ACOS_1: 
  269.     case ATAN_1: case REAL_1: 
  270. #endif
  271.          T1=arg1(B1); 
  272.              if(!assign(&at1,T1)) goto notreduce;
  273.  
  274.     case MAXINT_0: case MININT_0: case MAXAR_0: case MAXDEP_0:
  275. #if  REALARITH
  276.     case E_0: case PI_0: 
  277. #endif
  278.  
  279.      break;
  280.  
  281.     default:goto notreduce;
  282.    }
  283.    if(compute(A,&at1,&at2,&atR,false))
  284.     {
  285. #if REALARITH
  286.       if(isreal(&atR)) return UNI(B0,mkreal(realf(&atR)));
  287. #endif
  288. #if LONGARITH
  289.       return LONGRES(B0,longf(&atR));
  290. #endif
  291. #if !LONGARITH
  292.      return INTRES(B0,longf(&atR));
  293. #endif
  294.     }
  295.  
  296. notreduce:
  297.    if(eval)return false;
  298. termreduce:
  299.    UNI(B0,B1);
  300.    return true;
  301. }
  302.  
  303. /*
  304. #define push(v,t)        {name(HT)= (ATOM)v;son(HT)=t;\
  305.                   if(dec_term(HT)<=GLOTOP)ERROR(LOCALSPACEE);}
  306. #define pop()            {inc_term(HT);PVAR= (TERM)name(HT);\
  307.                   PTERM=son(HT);}
  308. */
  309. #define push(v,t)    {name(HT)=VART; val(HT)=v; dec_term(HT); \
  310.               name(HT)=VART; val(HT)=t;\
  311.                   if(dec_term(HT)<=GLOTOP)ERROR(LOCALSPACEE);}
  312. #define pop()  {inc_term(HT);PTERM=val(HT);inc_term(HT);PVAR=val(HT);}
  313.  
  314. LOCAL TERM NCP,PVAR,PTERM,HT;
  315.  
  316. LOCAL void nextp(TERM V)
  317. { name(PVAR)=VART; val(PVAR)=V;
  318.   pop();
  319. }
  320.  
  321. LOCAL void nextcall(TERM C)
  322. { NCP=mk2sons(name(C),son(C),GOTO_1,NCP);
  323.   pop();
  324. }
  325.  
  326. LOCAL void nexte(TERM C, TERM NV, TERM NT)
  327. { name(PVAR)=VART; val(PVAR)=son(C);
  328.   NCP=mk2sons(name(C),son(C),GOTO_1,NCP);
  329.   PVAR=NV; PTERM=NT; /* explicit pop */
  330. }
  331.  
  332. GLOBAL TERM DOEVAL(TERM CALLP, ENV ENVP)
  333. {
  334.   register TERM H;
  335.   TERM HH,H1,H2,ONCP;
  336.   ATOM AA1,AA2,PA,CA;
  337.   int i;
  338.   TERM T1,T2;
  339.  
  340.   ONCP=NCP=br(CALLP);
  341.   E=ENVP; 
  342.   BE=base(ENVP);
  343.   PTERM=mkfreevar(); UNI(PTERM,arg2(CALLP));
  344.   PVAR=arg1(CALLP);
  345.   HT=HEAPTOP;
  346.   while(HT <=HEAPTOP)
  347.   { deref(PTERM);
  348.     if((PA=name(PTERM))<NORMATOM)
  349.         { nextp(PTERM); continue; }
  350.     CA=copyatom(LOOKATOM(PA,arity(PA)+1));
  351.     if(non_nil_clause(clause(CA)) ||
  352.       class(CA)==EVALP || class(CA)==BTEVALP)
  353.       { /* executable function f(X,a1,...,aN) */
  354.         if(!arity(PA) && non_nil_clause(clause(CA)) 
  355.           && name(body(clause(CA)))==nil_atom)
  356.            /* direct access to the value of simple global variables */
  357.            { nextp(son(head(clause(CA)))); continue; }
  358.         H1=stackterms(arity(CA)); name(H1)=VART; son(H1)=PVAR;
  359.         H2=br(H1); H=son(PTERM);
  360.         for(i=0;i<arity(PA);i++)
  361.         {
  362.           name(H2)=VART;son(H2)=H;
  363.           next_br(H2);next_br(H);
  364.         }
  365.         /* putcall: f(X,a1,..,aN) ; X=f(a1,..,aN)  */
  366.         nextcall(mkfunc(SEMI_2, mk2sons(CA,H1,
  367.                   ISEQ_2, mk2sons(VART,PVAR,VART,PTERM))));
  368.         continue;
  369.       }
  370.           
  371.     switch(PA)
  372.     {
  373. #if REALARITH
  374.          case PI_0: nextp(mkreal(PI_CONST));break;
  375.          case E_0: nextp(mkreal(E_CONST));break;
  376. #endif
  377.          case MAXAR_0: nextp(mkint(MAXARITY));break;
  378.          case MAXDEP_0: nextp(mkint(MAXDEPTH));break;
  379. #if LONGARITH
  380.          case MAXINT_0: nextp(mklong(maxlong));break;
  381.          case MININT_0: nextp(mklong(minlong));break;
  382. #endif
  383. #if ! LONGARITH
  384.          case MAXINT_0: nextp(mkint(maxint));break;
  385.          case MININT_0: nextp(mkint(minint));break;
  386. #endif
  387.  
  388.      case MINUS_1: case BITNEG_1: case NEG_1: 
  389. #if REALARITH
  390.      case FLOOR_1: case CEIL_1: case ENTIER_1: case EXP_1: 
  391.      case LN_1: case LOG10_1: case SQRT_1: case SIN_1: 
  392.      case COS_1: case TAN_1: case ASIN_1: case ACOS_1:
  393.      case ATAN_1:  case REAL_1:
  394. #endif 
  395.               T1=arg1(PTERM);
  396.               AA1=name(T1);
  397.               if(is_number(AA1))
  398.                { DOREDUCE(PVAR,PTERM,true); pop(); }
  399.               else 
  400.                { H1=mkfreevar();
  401.                 nexte(mkfunc(REDUCE_2,
  402.                        mk2sons(UNBOUNDT,nil_term,PA,H1)),H1,T1);
  403.                 }
  404.               break;
  405.  
  406.  
  407.     case PLUS_2: case MINUS_2: case TIMES_2: 
  408.     case LSHIFT_2: case RSHIFT_2: case BITAND_2: 
  409.     case BITOR_2: case AND_2: case OR_2: case IDIV_2: case MOD_2:  
  410. #if REALARITH
  411.     case DIVIDE_2:  case POWER_2: 
  412. #endif 
  413.            T1=arg1(PTERM); T2=arg2(PTERM);
  414.            AA1=name(T1); AA2=name(T2);
  415.            if(is_number(AA1))
  416.               if(is_number(AA2))
  417.                 { DOREDUCE(PVAR,PTERM,true); pop(); }
  418.               else
  419.                { H2=mkfreevar();
  420.                  nexte(mkfunc(REDUCE_2,mk2sons(UNBOUNDT,nil_term,PA,
  421.                           mk2sons(AA1,son(T1),VART,H2))),H2,T2);
  422.                 }
  423.            else
  424.               if(is_number(AA2))
  425.                 {H1=mkfreevar();
  426.                  nexte(mkfunc(REDUCE_2,mk2sons(UNBOUNDT,nil_term,PA,
  427.                           mk2sons(VART,H1,name(T2),son(T2)))),H1,T1);
  428.                 }
  429.               else
  430.                 {H1=mkfreevar(); H2=mkfreevar();
  431.                  nexte(mkfunc(REDUCE_2,mk2sons(UNBOUNDT,nil_term,PA,
  432.                           mk2sons(VART,H1,VART,H2))),H1,T1);
  433.                  push(H2,T2);
  434.                 }
  435.            break;
  436.  
  437. #if SYMBOLARITH
  438.         case SUBST_3:
  439.            { TERM jj,j; 
  440.               j=jj=stackterms(2);
  441.               T1=arg2(PTERM); T2=arg3(PTERM);
  442.               while(name(T1)==CONS_2 && name(T2)==CONS_2)
  443.                 { 
  444.                   name(jj)=name(arg1(T1)); son(jj)=nil_term;
  445.           next_br(jj); name(jj)=VART; son(jj)=arg1(T2);
  446.                   jj=stackterms(2); T1=arg2(T1);T2=arg2(T2);
  447.                 }
  448.               if(name(T1)!=NIL_0 || name(T2) !=NIL_0)goto noteval;
  449.               name(jj)=nil_atom; son(jj)=nil_term;
  450.               H1=mkfreevar();
  451.               nextp(substsim(arg1(PTERM),j));
  452.               break;
  453.            }
  454.  
  455.     /* constructor operations */
  456.         case LAMBDA_1:
  457.         case INL_1:
  458.         case INR_1:
  459.         case COMMA_2:
  460.         case CONS_2:
  461.         case NIL_0:
  462.            goto noteval;
  463.             case PIND_3:
  464.                nextp(pind3_red(PTERM));break;
  465.             case OF_2:
  466.                nextp(of_red(PTERM));break;
  467.  
  468.     /* selector operations */
  469.             case QUOTE_1:
  470.         case EVAL_1: 
  471.         case SUCC_1:
  472.         case PRED_1:
  473.         case SPREAD_2:
  474.         case LISTIND_3:
  475.         case IND_4:
  476.         case INT_EQ_4:
  477.         case DECIDE_3:
  478.         case RECIND_3:
  479.                nextp(symbred(PTERM));break;
  480. #endif
  481.  
  482.         default:
  483.         noteval:
  484.                nextp(PTERM);
  485.     }/* switch */
  486.    } /* while */
  487.  /* erase simple reduce-calls */
  488.  /* restore first callp for trace only */
  489.   H=NCP;
  490.   H1=NCP=mk2sons(name(CALLP),son(CALLP),GOTO_1,NCP);
  491.   while(H !=ONCP)
  492.   { if(name(H)==REDUCE_2)
  493.       {
  494.        HH=arg2(H);
  495.        if(DOREDUCE(son(H),HH,true))
  496.          son(br(H1))=son(br(H));
  497.        else
  498.          H1=H;
  499.       }
  500.     next_br(H); H=son(H); /* H=son(br(H));*/
  501.   }
  502.   return NCP;
  503. }
  504.  
  505. LOCAL void iseval(TERM t, ARITHTYPE *ap)
  506. {
  507.   ARITHTYPE at1,at2;
  508.   register TERM s;
  509.   ATOM a;
  510.  
  511.    if(ISDEPTH++ > MAXDEPTH){ISDEPTH=0;ERROR(DEPTHE);}
  512. #if REALARITH
  513.    isreal(ap)=isreal(&at1)=isreal(&at2)=false;
  514. #endif
  515.    if((a=name(t))<NORMATOM) if(assign(ap,t))goto ret;
  516.                         else ERROR(STDFUNCARGE);
  517.    switch(arity(a))
  518.    { 
  519.      case 2: s=arg2(t); if(!assign(&at2,s)) iseval(s,&at2);
  520.      case 1: s=arg1(t); if(!assign(&at1,s)) iseval(s,&at1);
  521.      case 0: break;
  522.      default:ERROR(UNDEFFUNCE);
  523.    }
  524.      (void)compute(a,&at1,&at2,ap,true);
  525. ret: ISDEPTH--;
  526.     return;
  527. }
  528.  
  529. /* returns integer-result of evaluation of expression T */
  530. GLOBAL int INTVALUE(TERM T)
  531. { ARITHTYPE a;
  532.   deref(T);iseval(T,&a);
  533. #if REALARITH && LONGARITH
  534.   if(isreal(&a) || (maxint < longf(&a)) || (minint > longf(&a))) 
  535.                 ERROR(BADEXPE);  
  536. #endif
  537. #if REALARITH && ! LONGARITH
  538.   if(isreal(&a)) ERROR(BADEXPE);  
  539. #endif
  540. #if ! REALARITH && LONGARITH
  541.   if((maxint < longf(&a)) || (minint > longf(&a))) ERROR(BADEXPE);  
  542. #endif
  543.   return (int)longf(&a);
  544. }
  545.  
  546. #if SYMBOLARITH
  547. GLOBAL TERM SUBSTITUTION(TERM X, TERM V, TERM T)
  548. {
  549.      TERM LL,L; 
  550.       L=LL=stackterms(2);
  551.       while(name(V)==CONS_2 && name(T)==CONS_2)
  552.     { 
  553.       name(LL)=name(arg1(V)); son(LL)=nil_term;
  554.       next_br(LL); name(LL)=VART; son(LL)=arg1(T);
  555.       LL=stackterms(2); V=arg2(V);T=arg2(T);
  556.     }
  557.       if(name(V)!=NIL_0 || name(T) !=NIL_0) ARGERROR();
  558.       name(LL)=nil_atom; son(LL)=nil_term;
  559.       return substsim(X,L);
  560. }
  561. #endif
  562.  
  563. GLOBAL boolean DOACOMP(void)
  564. {
  565. #if REALARITH
  566.   REAL R1,R2;
  567.   boolean is_real=false;
  568. #endif
  569. #if LONGARITH
  570.   LONG L1,L2;
  571. #endif
  572. #if !LONGARITH
  573.   int L1,L2;
  574. #endif
  575.  TERM H1,H2;
  576.  boolean is_term1=false,is_term2=false;
  577.  
  578.  CALLX=A0; 
  579.  H1=arg1(A0); H2=arg2(A0);
  580. #if REALARITH && LONGARITH
  581.  switch(name(H1))
  582.   { 
  583.     case REALT:   R1=realval(H1);is_real=true;break;
  584.     case INTT:    R1= (REAL)(L1= (LONG)ival(H1));break;
  585.     case LONGT:   R1= (REAL)(L1=longval(H1));break;
  586.     case 0: default: is_term1=true;
  587.   }
  588.  switch(name(H2))
  589.   { 
  590.     case REALT:   R2=realval(H2);is_real=true;break;
  591.     case INTT:    R2= (REAL)(L2= (LONG)ival(H2));break;
  592.     case LONGT:   R2= (REAL)(L2=longval(H2));break;
  593.     case 0: default: is_term2=true; 
  594.   }
  595. #endif
  596. #if REALARITH && ! LONGARITH
  597.  switch(name(H1))
  598.   { 
  599.     case REALT:   R1=realval(H1);is_real=true;break;
  600.     case INTT:    R1= (REAL)(L1=ival(H1));break;
  601.     case 0: default: is_term1=true;
  602.   }
  603.  switch(name(H2)) 
  604.   { 
  605.     case REALT:   R2=realval(H2);is_real=true;break; 
  606.     case INTT:    R2= (REAL)(L2=ival(H2));break;
  607.     case 0: default: is_term2=true;
  608.   }
  609. #endif
  610. #if ! REALARITH && LONGARITH
  611.  switch(name(H1))
  612.   { 
  613.     case INTT:    L1= (LONG)ival(H1);break;
  614.     case LONGT:   L1=longval(H1);break;
  615.     case 0: default: is_term1=true;
  616.   }
  617.  switch(name(H2))
  618.   { 
  619.     case INTT:    L2= (LONG)ival(H2);break;
  620.     case LONGT:   L2=longval(H2);break;
  621.     case 0: default: is_term2=true;
  622.   }
  623. #endif
  624. #if ! REALARITH && ! LONGARITH
  625.  if (name(H1)==INTT) L1=ival(H1); else is_term1=true;
  626.  if (name(H2)==INTT) L2=ival(H2); else is_term2=true;
  627. #endif
  628. #if REALARITH
  629. if(is_real)
  630.  switch(name(A0))
  631.  {
  632.    default: ARGERROR();
  633.    case EQ_2: if (is_term1 || is_term2) return UNI(H1,H2); 
  634.           return R1==R2;
  635.    case NE_2: if (is_term1 || is_term2) return !UNI(H1,H2);
  636.           return R1 !=R2;
  637.    case GT_2: if (is_term1 || is_term2) ARGERROR();
  638.           return R1 > R2;
  639.    case LT_2: if (is_term1 || is_term2) ARGERROR();
  640.           return R1 < R2;
  641.    case GE_2: if (is_term1 || is_term2) ARGERROR();
  642.           return R1 >=R2;
  643.    case LE_2: if (is_term1 || is_term2) ARGERROR();
  644.           return R1 <=R2;
  645.  }
  646. #endif
  647.  switch(name(A0))
  648.  {
  649.    default: ARGERROR();
  650.    case EQ_2: if (is_term1 || is_term2) return UNI(H1,H2);
  651.           return L1==L2;
  652.    case NE_2: if (is_term1 || is_term2) return !UNI(H1,H2);
  653.           return L1 !=L2;
  654.    case GT_2: if (is_term1 || is_term2) ARGERROR();
  655.           return L1 > L2;
  656.    case LT_2: if (is_term1 || is_term2) ARGERROR();
  657.           return L1 < L2;
  658.    case GE_2: if (is_term1 || is_term2) ARGERROR();
  659.           return L1 >=L2;
  660.    case LE_2: return L1 <=L2;
  661.  }
  662. }
  663.  
  664. GLOBAL boolean DOIS(TERM L, TERM R)
  665. { ARITHTYPE a;
  666.   iseval(R,&a);
  667. #if REALARITH
  668.   if(isreal(&a)) return UNI(L,mkreal(realf(&a)));
  669. #endif
  670. #if LONGARITH
  671.   return LONGRES(L,longf(&a));
  672. #endif
  673. #if ! LONGARITH
  674.   return INTRES(L,longf(&a));
  675. #endif
  676. }
  677.  
  678. GLOBAL boolean DODASS(void)
  679. {
  680. static TERM DEST,T,RT,H1,H2,H;
  681. static CLAUSE CL,CLL;
  682. static ATOM AT,AT1;
  683. int ARITY;
  684. static boolean DONE;
  685.   if(name(A0) < NORMATOM)  return UNI(A0,A1); 
  686.   DEST=A0;
  687.   DONE=false;
  688.   CLL=nil_term;
  689.   AT=name(DEST);  
  690.   ARITY=arity(AT)+1;
  691.   if (ARITY==1) RT=mkatom(AT);
  692.   AT1=copyatom(LOOKATOM(AT,ARITY));
  693.   for(CL=clause(AT1);non_nil_clause(CL);) 
  694.     if(name(body(CL))==nil_atom)
  695.       { T=head(CL); 
  696.         if (ARITY>1) RT=mkfunc(AT,br(son(T)));
  697.         if(DOEQUAL(RT,DEST,MAXDEPTH))
  698.            if(DONE)
  699.              { CLAUSE CL0;
  700.            CL0=nextcl(CL);
  701.                if(non_nil_clause(CLL)) nextcl(CLL)=CL0;
  702.                else clause(AT1)=CL0;
  703.                if(testheap(CL)) notecl(CL); else destroycl(CL);
  704.            CL=CL0;
  705.               }
  706.            else
  707.              {
  708.                DONE=true;
  709.                H1=son(T); 
  710.                if(name(H1)>FUNCNAME)
  711.                    freeterms(arity(name(H1)),son(H1));
  712.                if((name(H1)=name(A1))==INTT)
  713.                     { ival(H1)=ival(A1); }
  714.                else { VARTOP=VARCT=0;
  715.                       son(H1)=SKELETON(name(A1),son(A1)); }
  716.            CLL=CL; CL=nextcl(CL);
  717.               }
  718.     else { CLL=CL; CL=nextcl(CL); }
  719.        }
  720.   if(DONE)return true;
  721.   H1=stackterms(ARITY); name(H1)=VART; val(H1)=A1;
  722.   H2=br(H1); H=son(DEST);
  723.   while(--ARITY>0)
  724.     { name(H2)=VART;son(H2)=H; H2=br(H2); H=br(H); }
  725.   A0=mkfunc(AT1,H1);
  726.   CL=ADDCLAUSE(A0);
  727.   nextcl(CL)=clause(AT1); clause(AT1)=CL;
  728.   return true;
  729. }
  730.  
  731. #if SYMBOLARITH
  732.  
  733. LOCAL TERM MAC_HLP;
  734.  
  735. LOCAL TERM mkl1(ATOM AT1, TERM S1)
  736. {   TERM H,H1;
  737.     H1=H=stackterms(3);
  738.     name(H1)=AT1;son(H1)=nil_term;
  739.     next_br(H1); name(H1)=VART; son(H1)=S1;
  740.     next_br(H1); name(H1)=nil_atom;son(H1)=nil_term; 
  741.     return H;
  742. }
  743.  
  744. LOCAL TERM mkl2(ATOM AT1, TERM S1, ATOM AT2, TERM S2)
  745. {   register TERM H,H1;
  746.     H1=H=stackterms(5);
  747.     name(H1)=AT1; son(H1)=nil_term;
  748.     next_br(H1); name(H1)=VART; son(H1)=S1;
  749.     next_br(H1); name(H1)=AT2; son(H1)=nil_term;
  750.     next_br(H1); name(H1)=VART; son(H1)=S2;
  751.     next_br(H1); name(H1)=nil_atom; son(H1)=nil_term;
  752.     return H;
  753. }
  754.  
  755. LOCAL TERM mkl3(ATOM AT1, TERM S1, ATOM AT2, TERM S2, ATOM AT3, 
  756.                 TERM S3)
  757. {   register TERM H,H1;
  758.     H1=H=stackterms(7);
  759.     name(H1)=AT1; son(H1)=nil_term;
  760.     next_br(H1); name(H1)=VART; son(H1)=S1;
  761.     next_br(H1); name(H1)=AT2; son(H1)=nil_term;
  762.     next_br(H1); name(H1)=VART; son(H1)=S2;
  763.     next_br(H1); name(H1)=AT3; son(H1)=nil_term;
  764.     next_br(H1); name(H1)=VART; son(H1)=S3;
  765.     next_br(H1); name(H1)=nil_atom; son(H1)=nil_term;
  766.     return H;
  767. }
  768.  
  769. #define getbound(A,HH)  if (name(HH)!=COLON_2) return H;\
  770.                         A=name(arg1(HH));\
  771.                         if (arity(A)||A<NORMATOM) return H;\
  772.                         HH=arg2(HH);
  773.  
  774. #define check2(HH,C)    if(C) {HH=symbred(HH);if(C) break;}
  775.  
  776. TERM symbred(TERM H)
  777.   { TERM H1,H2;
  778.     ATOM N,N1,N2;
  779.     deref(H);
  780.     N=name(H);
  781.     switch(N)
  782.     {
  783.       case INTT:
  784.       case UNBOUNDT:
  785.            return H;
  786.       case RECIND_3:
  787.            H1=arg1(H);
  788.        check2(H1,name(H1)!=INL_1 && name(H1)!=INR_1);
  789.            if(name(H1)==INL_1)
  790.            { H2=arg2(H);
  791.          getbound(N1,H2);
  792.              return symbred(substsim(H2,mkl1(N1,arg1(H1))));
  793.            }
  794.            if(name(H1)==INR_1)
  795.            { TERM T;
  796.              H2=arg3(H);
  797.          getbound(N1,H2);
  798.          getbound(N2,H2);
  799.              T=stackterms(3);
  800.              name(T)=N1; son(T)=nil_term; 
  801.              name(br(T))=COLON_2; son(br(T))=son(arg2(H));
  802.              name(br(br(T)))=COLON_2; son(br(br(T)))=son(arg3(H));
  803.          H=mkfunc(LAMBDA_1,
  804.                   mkfunc(COLON_2,mk2sons(N1,nil_term,RECIND_3,T)));
  805.              return substsim(H2,mkl2(N1,H,N2,arg1(H1)));
  806.            }
  807.       case QUOTE_1:
  808.            return arg1(H); 
  809.       case EVAL_1:
  810.            return symbred(symbred(arg1(H))); 
  811.       case OF_2: 
  812.        return of_red(H);
  813.       case SPREAD_2:
  814.            H1=arg1(H);
  815.        check2(H1,name(H1)!=COMMA_2);
  816.            H2=arg2(H);
  817.        getbound(N1,H2);
  818.        getbound(N2,H2);
  819.            H=substsim(H2,mkl2(N1,arg1(H1),N2,arg2(H1)));
  820.            break;
  821.      case DECIDE_3:
  822.            H1=arg1(H);
  823.        check2(H1,name(H1)!=INL_1 && name(H1)!=INR_1);
  824.            if(name(H1)==INL_1)H2=arg2(H);
  825.            else H2=arg3(H);
  826.        getbound(N1,H2);
  827.            H=substsim(H2,mkl1(N1,arg1(H1)));
  828.            break;
  829.     case COMMA_2:
  830.     case CONS_2:
  831.            return mkfunc(N,mk2sons(VART,symbred(arg1(H)),VART,symbred(arg2(H))));
  832.     case LAMBDA_1:
  833.     case NIL_0: 
  834.        return H;
  835.     case SUCC_1:
  836.        H=symbred(arg1(H));
  837.        if (name(H)==PRED_1) return arg1(H); 
  838.        /* else if (name(H)==INTT) H=mkint(ival(H)+1); */
  839.            else return mkfunc(SUCC_1,mkfunc(VART,H));
  840.     case PRED_1:
  841.        H=symbred(arg1(H));
  842.        if (name(H)==SUCC_1) return arg1(H); 
  843.        /* else if (name(H)==INTT) H=mkint(ival(H)-1); */
  844.            return mkfunc(PRED_1,mkfunc(VART,H));
  845.     case INL_1:
  846.     case INR_1:
  847.            return mkfunc(N,mkfunc(VART,symbred(arg1(H))));
  848.     case INT_EQ_4:
  849.       { TERM L,R,T;
  850.     L=symbred(arg1(H)); R=symbred(arg2(H));
  851.     if (name(L)==INTT && name(R)==INTT)
  852.     { if (ival(L)==ival(R)) H=symbred(arg3(H)); 
  853.       else H=symbred(arg4(H));
  854.       break;
  855.     }
  856.     T=H1=stackterms(4);
  857.     name(H1)=VART; val(H1)=L; next_br(H1);
  858.     name(H1)=VART; val(H1)=R; next_br(H1);
  859.     name(H1)=VART; val(H1)=arg3(H); next_br(H1);
  860.     name(H1)=VART; val(H1)=arg4(H); 
  861.         return mkfunc(N,T);
  862.       }
  863.     case IND_4:
  864.       { ATOM LAST,I;
  865.         TERM desc;
  866.         int n, ii, sign;
  867.            H1=arg1(H);
  868.        check2(H1,name(H1)!=INTT);
  869.            ii=ival(H1);
  870.            if(ii==0) return symbred(arg3(H)); 
  871.            if(ii<0){ desc=arg2(H); sign= -1; }
  872.            else { desc=arg4(H); sign=1; }
  873.        getbound(I,desc);
  874.        getbound(LAST,desc);
  875.            H=arg3(H);
  876.            H2=mkint(98);
  877.            for(n=1;n<=ii;n +=sign)
  878.             {
  879.              ival(H2)=n;
  880.              H=substsim(desc,mkl2(LAST,H,I,H2));
  881.              if(name(H) > NORMATOM && DOREDUCE(H1=mkfreevar(),H,true))
  882.                     {H=H1;deref(H);}
  883.             }
  884.            return H;
  885.            break;
  886.       }
  887.  
  888.      case PIND_3: return pind3_red(H); 
  889.  
  890.      case LISTIND_3:
  891.       {ATOM N3;
  892.        TERM ST,HH;
  893.         H1=arg1(H);
  894.         if(name(H1)==NIL_0) return arg2(H); 
  895.         if(name(H1)!=CONS_2)
  896.         {
  897.           H1=symbred(H1);
  898.       if(name(H1)==NIL_0) return arg2(H);
  899.           if(name(H1)!=CONS_2) return H;
  900.         }
  901.         H2=arg3(H);
  902.     getbound(N1,H2);
  903.     getbound(N2,H2);
  904.     getbound(N3,H2);
  905.         HH=ST=stackterms(1);
  906.         while(name(H1)==CONS_2)
  907.         {
  908.           son(ST)=H1;
  909.           H1=arg2(H1); ST=stackterms(1);
  910.         }
  911.         dec_term(ST);
  912.         if(name(H1)==NIL_0)H=arg2(H);
  913.         else
  914.          { TERM T;/*  fehler!!!!! */
  915.           T=stackterms(3);
  916.           name(T)=name(br(T))=name(br(br(T)))=VART;
  917.           son(T)=H1; son(br(T))=arg2(H);
  918.           son(br(br(T)))=arg3(H);
  919.           H=mkfunc(LISTIND_3,T);
  920.          }
  921.         while(ST >=HH)
  922.         {
  923.           H=substsim(H2,mkl3(N1,arg1(son(ST)),  /* list head */
  924.                               N2,arg2(son(ST)),  /* list rest */
  925.                               N3,H)              /* rec.value */
  926.                      );
  927.           dec_term(ST);
  928.         }
  929.         break;
  930.        }
  931.      default:
  932.            if(arity(N)==0)
  933.            { N1=LOOKATOM(N,1);
  934.             if(clause(N1) && !name(body(clause(N1))))
  935.              { H=mkfreevar();
  936.                UNI(H,son(head(clause(N1))));
  937.                deref(H); return H;
  938.              }
  939.            }
  940.     }
  941. eret:
  942.   H1=mkfreevar();
  943.   if(name(H) > NORMATOM && DOREDUCE(H1,H,true))
  944.       {H=H1; deref(H);}
  945.   return H;
  946. }
  947.  
  948. GLOBAL boolean appears(ATOM A, int N, TERM T)
  949. { register TERM X;
  950.   register ATOM AA;
  951.   while(N-->0)
  952.   { X=T; deref(X); 
  953.     if((AA=name(X))==A) return true;
  954.     if(AA==COLON_2 && name(arg1(X))==A) return false;
  955.     if(AA>NORMATOM && arity(AA))
  956.       if(appears(A,arity(AA),son(X))) return true;
  957.     next_br(T);
  958.   }
  959.   return false;
  960. }
  961.  
  962. TERM substsim(TERM T, TERM L)
  963. /* short list */
  964. { register TERM H,H1;
  965.   int I;
  966.   register TERM HL;
  967.   ATOM N,NN;
  968.    deref(T);
  969.    if(!name(L)){H=T;goto ende;}
  970.    if((N=name(T)) < NORMATOM) return T;
  971.    if(arity(N)==0) 
  972.      {   HL=L;
  973.          while(name(HL))
  974.            {
  975.              if(name(HL) !=N) { next_br(HL); next_br(HL); }
  976.              else
  977.                { next_br(HL); H=mkfunc(VART,son(HL));
  978.                  goto ende;
  979.                }
  980.            }
  981.          H=  T; goto ende;
  982.      }
  983.    if(N==COLON_2)
  984.      { ATOM N0; TERM LL;
  985.        if((N=name(arg1(T))) > NORMATOM && arity(N)==0)
  986.        { if (N!=TILDE_0)
  987.       { LL=L; NN=N;
  988.         next_atom:
  989.         while(N0=name(LL))
  990.         { while(N==N0 || appears(N,1,son(LL))) 
  991.                     { N=modify(N); LL=L; goto next_atom; }
  992.           next_br(LL); next_br(LL);
  993.         }
  994.           }
  995.      if(N!=NN &&  N!=TILDE_0) /* renaming NN --> N */
  996.         T=substsim(arg2(T),mkl1(NN,mkatom(N)));
  997.      else T=arg2(T);
  998.      T=mkfunc(COLON_2,mk2sons(N,nil_term,VART,substsim(T,L)));
  999.          return T;
  1000.        }
  1001.        N=COLON_2;
  1002.      }
  1003.    T=son(T); H=H1=stackterms(arity(N));
  1004.    I=arity(N);
  1005.    for(;;)
  1006.     { ATOM A;
  1007.       register TERM TT;
  1008.       TT=T; deref(TT);
  1009.       if((A=name(TT))<NORMATOM){ name(H1)=VART;son(H1)=TT;goto cont;}
  1010.       if(arity(A)==0) 
  1011.          {   HL=L;
  1012.              while(non_nil_atom(name(HL)))
  1013.                {
  1014.                  if(name(HL)!=A) { next_br(HL); next_br(HL); }
  1015.                  else
  1016.                    { next_br(HL);
  1017.              name(H1)=VART;
  1018.                      son(H1)=son(HL);
  1019.                      goto cont;
  1020.                    }
  1021.                }
  1022.              name(H1)=A; son(H1)=nil_term;
  1023.              goto cont;
  1024.          }
  1025.       else {name(H1)=VART; son(H1)=substsim(TT,L);}
  1026. cont:
  1027.       if(--I==0) break;
  1028.       next_br(H1);next_br(T); 
  1029.     }
  1030.    H=mkfunc(N,H);
  1031. ende:
  1032.    deref(H);
  1033.    if (!REDUCEFLAG) goto ret;
  1034.    N=name(H); if(arity(N)) NN=name(arg1(H)); 
  1035.    if(N==LISTIND_3 && (NN==CONS_2 || NN==NIL_0)) goto redret;
  1036.    if(N==PIND_3 && (NN==SUCC_1 || NN==INTT)) return pind3_red(H);
  1037.    if(N==IND_4 && NN==INTT) goto redret;
  1038.    if(N==INT_EQ_4 && NN==INTT && name(arg2(H))==INTT) goto redret;
  1039.    /* !!!!!! pfui !!!!!!! */
  1040.    if(N==OF_2 && name(symbred(arg1(H)))==LAMBDA_1) return of_red(H);
  1041.    if(N==SPREAD_2 && NN==COMMA_2) goto redret;
  1042.    if(N==DECIDE_3 && (NN==INL_1 || NN==INR_1)) goto redret;
  1043.    if(N==RECIND_3 && (NN==INL_1 || NN==INR_1)) goto redret;
  1044.    if(N==EVAL_1 || N==QUOTE_1) goto redret;
  1045.   H1=mkfreevar();
  1046.   if(name(H) > NORMATOM && DOREDUCE(H1,H,true))
  1047.       {H=H1; deref(H);}
  1048.    goto ret;
  1049. redret: 
  1050.    H=symbred(H);
  1051. ret:
  1052.    return H;
  1053. }
  1054.  
  1055. LOCAL TERM pind3_red(register TERM H)
  1056. { TERM ST,HH;
  1057.   TERM H1,H2;
  1058.   ATOM N1,N2;
  1059.   /* deref(H); */
  1060.   H1=arg1(H); 
  1061.   if(name(H1)==INTT && ival(H1)>=0)
  1062.   if (ival(H1)==0) return arg2(H); 
  1063.   else { }
  1064.   if(name(H1)!=SUCC_1) 
  1065.   { H1=symbred(H1);
  1066.     if(name(H1)==INTT) 
  1067.       if (ival(H1)==0) return arg2(H); 
  1068.       else { }
  1069.     if(name(H1)!=SUCC_1) 
  1070.       { TERM T;  /* no further reduction */
  1071.         T=stackterms(3);
  1072.         name(T)=name(br(T))=name(br(br(T)))=VART;
  1073.         son(T)=H1; son(br(T))=arg2(H);
  1074.         son(br(br(T)))=arg3(H);
  1075.         return mkfunc(PIND_3,T); 
  1076.       }
  1077.   } 
  1078.   H2=arg3(H);
  1079.   /* getbound(N1,H2); */
  1080.   if (name(H2)!=COLON_2) return H;
  1081.   N1=name(arg1(H2));
  1082.   if (arity(N1)||N1<NORMATOM) return H;
  1083.   H2=arg2(H2);
  1084.  
  1085.   /* getbound(N2,H2); */
  1086.   if (name(H2)!=COLON_2) return H;
  1087.   N2=name(arg1(H2));
  1088.   if (arity(N2)||N2<NORMATOM) return H;
  1089.   H2=arg2(H2);
  1090.  
  1091.   HH=ST=stackterms(1);
  1092.   while(name(H1)==SUCC_1)
  1093.          { H1=arg1(H1); son(ST)=H1; ST=stackterms(1); }
  1094.   dec_term(ST);
  1095.   if(name(H1)==INTT && ival(H1)==0)  H=arg2(H); 
  1096.   else { TERM T;  /* no further reduction */
  1097.           T=stackterms(3);
  1098.           name(T)=name(br(T))=name(br(br(T)))=VART;
  1099.           son(T)=H1; son(br(T))=arg2(H);
  1100.           son(br(br(T)))=arg3(H);
  1101.           H=mkfunc(PIND_3,T); 
  1102.          }
  1103.   while(ST >=HH)
  1104.   { H=substsim(H2,mkl2(N1,son(ST),N2,H)); dec_term(ST); }
  1105.   H1=mkfreevar();
  1106.   if(name(H) > NORMATOM && DOREDUCE(H1,H,true))
  1107.       {H=H1; deref(H);}
  1108.   return H;
  1109. }
  1110.  
  1111. LOCAL TERM of_red(register TERM H)
  1112. { register TERM H1;
  1113.   register ATOM N;
  1114.   H1=arg1(H); 
  1115.   /* check2(H1,name(H1)!=LAMBDA_1); */
  1116.   if(name(H1)!=LAMBDA_1) 
  1117.    { H1=symbred(H1);
  1118.      if(name(H1)!=LAMBDA_1) goto ret;
  1119.    }
  1120.  
  1121.   H1=arg1(H1);
  1122.   /* getbound(N,H1); */
  1123.   if (name(H1)!=COLON_2) return H;
  1124.   N=name(arg1(H1));
  1125.   if (arity(N)||N<NORMATOM) return H;
  1126.   H=substsim(arg2(H1),mkl1(N,symbred(arg2(H))));
  1127. ret:
  1128.   H1=mkfreevar();
  1129.   if(name(H) > NORMATOM && DOREDUCE(H1,H,true)) {H=H1; deref(H);}
  1130.   return H;
  1131. }
  1132.  
  1133.  
  1134. #endif
  1135.  
  1136.  
  1137.